FLAT.LSP[W82,JMC]2 - www.SailDart.org

perm filename FLAT.LSP[W82,JMC]2 blob sn#641715 filedate 1982-02-16 generic text, type C, neo UTF8
COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	EKL Done.
C00015 ENDMK
C⊗;
EKL Done.
proof? 
* proof? 
* Done.
LISPAX read in 
proof? 
* FLAT started.
* 
* 
* 2. ∀X U.FLAT(X,U)=IF ATOM X THEN X~U ELSE FLAT(CAR X,FLAT(CDR X,U))
   deps: NIL

* 
* 
* 5. ∀X.FLATTEN(X)=IF ATOM X THEN LIST(X) ELSE FLATTEN(CAR X)*FLATTEN(CDR X)
   deps: NIL

* 
*  failed to derive 
∀X Y.(∀U.LISTP FLAT(X,U))∧(∀U.LISTP FLAT(Y,U))⊃(λX.TRUE)(X~Y)

cannot prove the following: 
(∀U.LISTP FLAT(Y18,U))∧(∀U.LISTP FLAT(X41,U))⊃(λX.TRUE)(X41~Y18)

*  failed to derive 
(∀U V.LISTP U*V)⊃(LISTP FLATTEN(X)∧LISTP FLATTEN(Y)⊃(λX.TRUE)(X~Y))

cannot prove the following: 
(∀U V.LISTP U*V)∧LISTP FLATTEN(Y)∧LISTP FLATTEN(X)⊃(λX.TRUE)(X~Y)

* 
* 8. (∀X Y.(∀U.FLAT(X,U)=FLATTEN(X)*U)∧(∀U.FLAT(Y,U)=FLATTEN(Y)*U)⊃
          (λX.TRUE)(X~Y))⊃(∀X U.FLAT(X,U)=FLATTEN(X)*U)
   deps: NIL

* 9. (∀U.FLAT(X,U)=FLATTEN(X)*U)∧(∀U.FLAT(Y,U)=FLATTEN(Y)*U)
   deps: (9)

* 10. FLAT(X,FLAT(Y,U))=FLAT(X,FLATTEN(Y)*U)
    deps: (9)

* 11. ∀U.FLAT(X,FLAT(Y,U))=FLAT(X,FLATTEN(Y)*U)
    deps: (9)

* 12. (∀U.FLAT(X,U)=FLATTEN(X)*U)∧(∀U.FLAT(Y,U)=FLATTEN(Y)*U)⊃
     (∀U.FLAT(X,FLAT(Y,U))=FLAT(X,FLATTEN(Y)*U))
    deps: NIL

* 13. ∀X Y.(∀U.FLAT(X,U)=FLATTEN(X)*U)∧(∀U.FLAT(Y,U)=FLATTEN(Y)*U)⊃
          (∀U.FLAT(X,FLAT(Y,U))=FLAT(X,FLATTEN(Y)*U))
    deps: NIL

*  failed to taut 
((∀X Y.(∀U.FLAT(X,U)=FLATTEN(X)*U)∧(∀U.FLAT(Y,U)=FLATTEN(Y)*U)⊃(λX.TRUE)(X~Y))⊃
  (∀X U.FLAT(X,U)=FLATTEN(X)*U))∧
(∀X Y.(∀U.FLAT(X,U)=FLATTEN(X)*U)∧(∀U.FLAT(Y,U)=FLATTEN(Y)*U)⊃
       (∀U.FLAT(X,FLAT(Y,U))=FLAT(X,FLATTEN(Y)*U)))⊃
 (∀X U.FLAT(X,U)=FLATTEN(X)*U)

cannot prove the following: 
(∀X1 Y1.(∀U4.FLAT(X1,U4)=FLATTEN(X1)*U4)∧(∀U4.FLAT(Y1,U4)=FLATTEN(Y1)*U4)⊃
         (∀U4.FLAT(X1,FLAT(Y1,U4))=FLAT(X1,FLATTEN(Y1)*U4)))⊃
 (∀X1 Y1.(∀U4.FLAT(X1,U4)=FLATTEN(X1)*U4)∧(∀U4.FLAT(Y1,U4)=FLATTEN(Y1)*U4)⊃
          (λX2.TRUE)(X1~Y1))∨(∀X1 U5.FLAT(X1,U5)=FLATTEN(X1)*U5)

* 14. (∀X.ATOM X⊃(∀U.FLAT(X,U)=FLATTEN(X)*U))∧
    (∀X Y.(∀U.FLAT(X,U)=FLATTEN(X)*U)∧(∀U.FLAT(Y,U)=FLATTEN(Y)*U)⊃
           (λX.TRUE)(X~Y))⊃(∀X U.FLAT(X,U)=FLATTEN(X)*U)
    deps: NIL

* 15. (∀X.ATOM X⊃(∀U.X~U=LIST(X)*U))∧
    (∀X Y.(∀U.FLAT(X,U)=FLATTEN(X)*U)∧(∀U.FLAT(Y,U)=FLATTEN(Y)*U)⊃
           (λX.TRUE)(X~Y))⊃(∀X U.FLAT(X,U)=FLATTEN(X)*U)
    deps: NIL

* 16. (∀X.ATOM X⊃(∀U.X~U=LIST(X)*U))∧
    (∀X Y.(∀U.FLAT(X,U)=FLATTEN(X)*U)∧(∀U.FLAT(Y,U)=FLATTEN(Y)*U)⊃
           (λX.TRUE)(X~Y))⊃(∀X U.FLAT(X,U)=FLATTEN(X)*U)
    deps: NIL

* 17. (∀X.TRUE)∧
    (∀X Y.(∀U.FLAT(X,U)=FLATTEN(X)*U)∧(∀U.FLAT(Y,U)=FLATTEN(Y)*U)⊃
           (λX.TRUE)(X~Y))⊃(∀X U.FLAT(X,U)=FLATTEN(X)*U)
    deps: NIL

* 18. (∀X Y.(∀U.FLAT(X,U)=FLATTEN(X)*U)∧(∀U.FLAT(Y,U)=FLATTEN(Y)*U)⊃
           (λX.TRUE)(X~Y))⊃(∀X U.FLAT(X,U)=FLATTEN(X)*U)
    deps: NIL

* 19. (∀X Y.(∀U.FLAT(X,U)=FLATTEN(X)*U)∧(∀U.FLAT(Y,U)=FLATTEN(Y)*U)⊃
           (λX.TRUE)(X~Y))⊃(∀X U.FLAT(X,U)=FLATTEN(X)*U)
    deps: NIL

* 20. (∀X Y.(∀U.FLAT(X,U)=FLATTEN(X)*U)∧(∀U.FLAT(Y,U)=FLATTEN(Y)*U)⊃
           (λX.TRUE)(X~Y))⊃(∀X U.FLAT(X,U)=FLATTEN(X)*U)
    deps: NIL

* 21. (∀X.ATOM X⊃(∀U.LISTP IF ATOM X THEN X~U ELSE FLAT(CAR X,FLAT(CDR X,U))))∧
    (∀X Y.(∀U.LISTP FLAT(X,U))∧(∀U.LISTP FLAT(Y,U))⊃(λX.TRUE)(X~Y))⊃
     (∀X U.LISTP FLAT(X,U))
    deps: NIL

* 22. (∀X.ATOM X⊃(∀U.LISTP X~U))∧
    (∀X Y.(∀U.LISTP FLAT(X,U))∧(∀U.LISTP FLAT(Y,U))⊃(λX.TRUE)(X~Y))⊃
     (∀X U.LISTP FLAT(X,U))
    deps: NIL

* 23. (∀X.TRUE)∧(∀X Y.(∀U.LISTP FLAT(X,U))∧(∀U.LISTP FLAT(Y,U))⊃(λX.TRUE)(X~Y))⊃
     (∀X U.LISTP FLAT(X,U))
    deps: NIL

* 24. (∀X Y.(∀U.LISTP FLAT(X,U))∧(∀U.LISTP FLAT(Y,U))⊃(λX.TRUE)(X~Y))⊃
     (∀X U.LISTP FLAT(X,U))
    deps: NIL

* 25. (∀X Y.(∀U.LISTP FLAT(X,U))∧(∀U.LISTP FLAT(Y,U))⊃(λX.TRUE)(X~Y))⊃
     (∀X U.LISTP FLAT(X,U))
    deps: NIL

* 26. (∀X Y.(∀U.LISTP FLAT(X,U))∧(∀U.LISTP FLAT(Y,U))⊃(λX.TRUE)(X~Y))⊃
     (∀X U.LISTP FLAT(X,U))
    deps: NIL

* 27. (∀X Y.(∀U.LISTP FLAT(X,U))∧(∀U.LISTP FLAT(Y,U))⊃(λX.TRUE)(X~Y))⊃
     (∀X U.LISTP FLAT(X,U))
    deps: NIL

*  failed to derive 
∀X Y.(∀U.LISTP FLAT(X,U))∧(∀U.LISTP FLAT(Y,U))⊃(λX.TRUE)(X~Y)

cannot prove the following: 
(∀U.LISTP FLAT(Y18,U))∧(∀U.LISTP FLAT(X41,U))⊃(λX.TRUE)(X41~Y18)

* 
;;;
(wipe-out)
(get-proofs lispax)
(proof flat)
(context lispax#1:*)

;;; flat(x,u) has an imbedded call which makes proofs more difficult.
(decl (flat) |ground⊗ground→ground| constant)

(axiom |∀x u.flat(x,u) = if atom x then x~u else flat(car x,flat(cdr x, u))|)
(lname definfo)

(decl (flatten) |ground → ground| constant)

(axiom |∀x.flatten(x) = if atom x then list(x)
                        else flatten(car x)*flatten(cdr x)|)
(lname definfo)

(∀E PHI |λX.∀U.LISTP FLAT(X,U)| sexpinduction
|nil*([1#1#1]($definfo**sortinfo))*nil*([1#2#1#2]($definfo**sortinfo))
**simpinfo*nil*([1](der))*nil|
 sortinfo)
 failed to derive 
∀X Y.(∀U.LISTP FLAT(X,U))∧(∀U.LISTP FLAT(Y,U))⊃(λX.TRUE)(X~Y)

cannot prove the following: 
(∀U.LISTP FLAT(Y18,U))∧(∀U.LISTP FLAT(X41,U))⊃(λX.TRUE)(X41~Y18)

* 

28. (∀X Y.(∀U.LISTP FLAT(X,U))∧(∀U.LISTP FLAT(Y,U))⊃(λX.TRUE)(X~Y))⊃
     (∀X U.LISTP FLAT(X,U))
    deps: NIL

* 
(∀E PHI |λX.∀U.LISTP FLAT(X,U)| sexpinduction
|nil*([1#1#1]($definfo**sortinfo))*nil*([1#2#1#2]($definfo**sortinfo))
**simpinfo*nil|
 sortinfo)

(∀e phi |λx.listp flatten(x)| sexpinduction
|nil*([1#1#1]($definfo*nil**simpinfo*nil))*nil
*([1#1#2](&definfo*nil**simpinfo*nil))*([1#1](imp(listappend)*der))*nil|
 sortinfo)
(lname listpflatten)

(∀e phi |λx.∀u.flat(x,u)=flatten(x)*u| sexpinduction
|nil*([1#1#1](&definfo*nil*$definfo**simpinfo*nil))*nil
*([1#1#2](&definfo**simpinfo*nil))|
listpflatten sortinfo)

(assume |(∀u.flat(x,u)=flatten(x)*u)∧(∀u.flat(y,u)=flatten(y)*u)|)

(trw |flat(x,flat(y,u))| |*-1| listpflatten sortinfo)

(∀i u)

(ci -3 -1)

(∀i (x y))

(trw |∀x u.flat(x,u) = flatten(x)*u| |imp(-6,-1)*taut|)

(∀e phi |λx.∀u.flat(x,u)=flatten(x)*u| sexpinduction
|nil|
listpflatten sortinfo)

(∀e phi |λx.∀u.flat(x,u)=flatten(x)*u| sexpinduction
|nil*([1#1#1](&definfo*$simpinfo*nil))|
listpflatten sortinfo)

(∀e phi |λx.∀u.flat(x,u)=flatten(x)*u| sexpinduction
|nil*([1#1#1](&definfo*$simpinfo*nil*$definfo*nil))|
listpflatten sortinfo)

(∀e phi |λx.∀u.flat(x,u)=flatten(x)*u| sexpinduction
|nil*([1#1#1](&definfo*$simpinfo*nil*$definfo**simpinfo*nil))|
listpflatten sortinfo)

(∀e phi |λx.∀u.flat(x,u)=flatten(x)*u| sexpinduction
|nil*([1#1#1](&definfo*$simpinfo*nil*$definfo**simpinfo*nil))*nil|
listpflatten sortinfo)

(∀e phi |λx.∀u.flat(x,u)=flatten(x)*u| sexpinduction
|nil*([1#1#1](&definfo*nil*$definfo**simpinfo*nil))*nil|
listpflatten sortinfo)

(∀e phi |λx.∀u.flat(x,u)=flatten(x)*u| sexpinduction
|nil*([1#1#1](&definfo*nil*$definfo**simpinfo*nil))*nil
*([1#1#2](&definfo**simpinfo))|
listpflatten sortinfo)

(∀E PHI |λX.∀U.LISTP FLAT(X,U)| sexpinduction
|nil*([1#1#1]($definfo**sortinfo))|
 sortinfo)

(∀E PHI |λX.∀U.LISTP FLAT(X,U)| sexpinduction
|nil*([1#1#1]($definfo**sortinfo*nil))|
 sortinfo)

(∀E PHI |λX.∀U.LISTP FLAT(X,U)| sexpinduction
|nil*([1#1#1]($definfo*nil**sortinfo*nil))|
 sortinfo)

(∀E PHI |λX.∀U.LISTP FLAT(X,U)| sexpinduction
|nil*([1#1#1]($definfo*nil**sortinfo*nil))*nil|
 sortinfo)

(∀E PHI |λX.∀U.LISTP FLAT(X,U)| sexpinduction
|nil*([1#1#1]($definfo*nil**sortinfo*nil))*nil
*([1#1#2]($definfo*nil*sortinfo*nil))|
 sortinfo)

(∀E PHI |λX.∀U.LISTP FLAT(X,U)| sexpinduction
|nil*([1#1#1]($definfo*nil**sortinfo*nil))*nil
*([1#1#2]($definfo*nil*sortinfo*nil))*nil|
 sortinfo)

(∀E PHI |λX.∀U.LISTP FLAT(X,U)| sexpinduction
|nil*([1#1#1]($definfo*nil**sortinfo*nil))*nil
*([1#1#2]($definfo*nil*sortinfo*nil))*sortinfo*nil|
 sortinfo)

;;;;
(∀E PHI |λX.∀U.LISTP FLAT(X,U)| sexpinduction
|nil*([1#1#1]($definfo**sortinfo))*nil*([1#2#1#2]($definfo**sortinfo))
**simpinfo*nil*([1](der))*nil|
 sortinfo)